import java.util.ArrayList;
import java.util.List;


public class Formula {

	private enum Tipo
	{
		NEGACAO, CONJUNCAO, DISJUNCAO, IMPLICACAO, EQUIVALENCIA, ATOMO
	}
	
	private Formula esquerda, direita;
	private Tipo operacao;
	private char atomo;
	
	private static String __tab;//so para usar no toString
	
	public Formula(String exp) throws Exception
	{
		Formula f = intepretar(exp);
		this.atomo = f.atomo;
		this.direita = f.direita;
		this.esquerda = f.esquerda;
		this.operacao = f.operacao;
	}
	
	public Formula(String exp, char[] conjuntoAlfa) throws Exception
	{
		Formula f = intepretar(exp, conjuntoAlfa);
		this.atomo = f.atomo;
		this.direita = f.direita;
		this.esquerda = f.esquerda;
		this.operacao = f.operacao;
	}
	
	public Formula()
	{
		esquerda = null;
		direita = null;
		operacao = null;
		atomo = '\0';
	}
	
	public static final char[] 
			CONJUNTO_ALFA_PADRAO = {'A', 'B', 'C', 'D', 'E', 'F', 'G', 'H', 'I', 'J', 'K',
				'L', 'M', 'N', 'O', 'P', 'Q', 'R', 'S', 'T', 'U', 'V', 'W', 'X', 'Y', 'Z'};
				
	private static char[] conjuntoAlfa = CONJUNTO_ALFA_PADRAO;
	
	public static final String[] 
			CONJUNTO_OMEGA_PADRAO = {"¬", "^", "v", "->", "<->"};
	
	/** Os simbolos sempre significam, nessa ordem, negação (indice 0), conjunção (indice 1), disjunção (indice 2), implicação (indice 3) e equivalencia (indice 4)*/
	private static String[] conjuntoOmega = CONJUNTO_OMEGA_PADRAO;
	
	private static Formula intepretar(String exp, char[] alfa) throws Exception
	{
		conjuntoAlfa = alfa;
		Formula f = intepretar(exp);
		conjuntoAlfa = CONJUNTO_ALFA_PADRAO;
		return f;
	}
	
	private static Formula intepretar(String exp) throws Exception
	{
		exp = exp.trim();
		
		if(exp.length() == 0) throw new Exception("Expressão vazia!");
		
		List<Tupla<Formula, Tipo>> termosAchados = new ArrayList<Tupla<Formula,Tipo>>();

		while(exp.length() > 0)
		{
			if(comecaComParenteses(exp))
			{
				if(exp.length() < 2) //tem algo mais alem do parentese?
					throw new Exception("Esperado um fecha-parenteses, mas trecho acaba antes! Trecho: \""+exp+"\"");
				
				exp = exp.substring(1).trim(); //pego o que esta logo apos o '('
				try
				{
					int i = indiceFechaParentesisCorrespondente(exp);
					Formula ff = intepretar(exp.substring(0, i)); //interpreta a formula dentro dos parenteses
					exp = exp.substring(i+1).trim(); //pego o que vem depois do ')', sem espaços desnecessarios
					if(exp.length() > 0) //tem algo mais depois de um termo entre parenteses?
					{
						if(comecaComOperadorBinario(exp)) //se tiver, deve ser um operador
						{
							String operador = operadorBinarioNoIncioDe(exp);
							exp = exp.substring(operador.length());//pego o que vem apos o operador
							termosAchados.add(new Tupla<Formula, Tipo>(ff, operacaoCorrespondenteA(operador)));//colocamos na lista de termos do mesmo nivel
							//apos isso, volta para o loop para achar outros termos no mesmo nivel
						}
						else throw new Exception("Esperado um operador binário! Trecho: \""+exp+"\""); //caso contrario esta errado
					}
					else //exp terminou com uma expressao entre parenteses
						termosAchados.add(new Tupla<Formula, Tipo>(ff, null)); //colocamos na lista de termos do mesmo nivel, sem operador pois é o ultimo
				}
				catch(Exception e)
				{
					throw new Exception("Problema ao procurar fecha-parenteses. Trecho: \""+exp+"\"\n"+e.getMessage());
				}
			}
			
			else if(serAtomo(exp.charAt(0)))
			{
				Formula ff = new Formula();
				ff.atomo = exp.charAt(0);
				ff.operacao = Tipo.ATOMO;
				exp = exp.substring(1).trim(); //pego o que vem depois do atomo, sem espaços desnecessarios
				
				if(exp.length() > 0) //tem algo mais depois de um atomo?
				{
					if(comecaComOperadorBinario(exp)) //se tiver, deve ser um operador
					{
						String operador = operadorBinarioNoIncioDe(exp);
						exp = exp.substring(operador.length());//pego o que vem apos o operador
						termosAchados.add(new Tupla<Formula, Tipo>(ff, operacaoCorrespondenteA(operador)));//colocamos na lista de termos do mesmo nivel
						//apos isso, volta para o loop para achar outros termos no mesmo nivel
					}
					else throw new Exception("Esperado um operador binário! Trecho: \""+exp+"\""); //caso contrario esta errado
				}
				else //exp terminou com uma expressao entre parenteses
					termosAchados.add(new Tupla<Formula, Tipo>(ff, null)); //colocamos na lista de termos do mesmo nivel, sem operador pois é o ultimo
			}
			else if(comecaComNegacao(exp))
			{
				Formula ff = new Formula();
				ff.operacao = Tipo.NEGACAO;
				exp = exp.substring(conjuntoOmega[0].length()); //pula o simbolo de negacao
				int i = indiceProximoOperadorPrecedenciaInferiorANegacao(exp);
				ff.esquerda = intepretar(exp.substring(0, i));
				exp = exp.substring(i).trim(); //pego o que vem depois do escopo da negacao, sem espaços desnecessarios
				
				if(exp.length() > 0) //tem algo mais depois do escopo da negacao?
				{
					if(comecaComOperadorBinario(exp)) //se tiver, deve ser um operador
					{
						String operador = operadorBinarioNoIncioDe(exp);
						exp = exp.substring(operador.length());//pego o que vem apos o operador
						termosAchados.add(new Tupla<Formula, Tipo>(ff, operacaoCorrespondenteA(operador)));//colocamos na lista de termos do mesmo nivel
						//apos isso, volta para o loop para achar outros termos no mesmo nivel
					}
					else throw new Exception("Esperado um operador binário! Trecho: \""+exp+"\""); //caso contrario esta errado
				}
				else //exp terminou com uma expressao entre parenteses
					termosAchados.add(new Tupla<Formula, Tipo>(ff, null)); //colocamos na lista de termos do mesmo nivel, sem operador pois é o ultimo
			}
			
			exp = exp.trim();
		}
		
		return arrumaTermosPorPrecedencia(termosAchados);
	}
	
	private static boolean comecaComParenteses(String exp)
	{
		return exp.charAt(0) == '(';
	}
	
	private static boolean serAtomo(char ch)
	{
		for(char c : conjuntoAlfa)
			if(c == ch) return true;
		return false;
	}
	
	private static boolean comecaComOperadorBinario(String exp)
	{
		if(operadorBinarioNoIncioDe(exp) == null) return false;
		else return true;
	}
	
	private static Tipo operacaoCorrespondenteA(String op)
	{
		for(int i = 1; i < conjuntoAlfa.length; i++)
			if(op.equals(conjuntoOmega[i])) switch(i)
			{
				case 1: return Tipo.CONJUNCAO;
				case 2: return Tipo.DISJUNCAO;
				case 3: return Tipo.IMPLICACAO;
				case 4: return Tipo.EQUIVALENCIA;
				default: return null; //não deveria acontecer
			}
		return null;
	}
	
	private static String operadorBinarioNoIncioDe(String exp)
	{
		for(int i = 1; i < conjuntoAlfa.length; i++)
			if(exp.startsWith(conjuntoOmega[i]))
			{
				return conjuntoOmega[i];
			}
		return null;
	}
	
	private static boolean comecaComNegacao(String exp)
	{
		return exp.startsWith(conjuntoOmega[0]);
	}
	
	private static int indiceProximoOperadorPrecedenciaInferiorANegacao(String exp)
	{
		String str = exp;
		do
		{
			for(int i = 1; i < conjuntoOmega.length; i++)
			{
				if(str.startsWith(conjuntoOmega[i]))
				{
					break;
				}
			}
			if(str.charAt(0) == '(')
			{
				int contaParenteses = 1;
				do
				{
					str = str.substring(1);
					if(str.charAt(0) == '(') contaParenteses++;
					else if(str.charAt(0) == ')') contaParenteses--;
					
				}while(contaParenteses != 0);
				
			}
			str = str.substring(1);
		}
		while(str.length() > 0);
		
		return exp.length()-str.length();
	}
	
	/** Retorna o indice do fecha parenteses correspondente ao nivel atual de escopo. O abre parentese deve estar omitido. 
	 * @throws Exception Quando não acha o parentese correspondente*/
	private static int indiceFechaParentesisCorrespondente(String subexp) throws Exception
	{
		int count=0;
		char[] array = subexp.toCharArray();
		for(int i = 0; i < array.length; i++)
		{
			if(array[i] == '(')
				count++;
			
			else if(array[i] == ')')
			{
				if(count == 0) return i;
				else count--;
			}	
		}
		throw new Exception("Indice nao encontrado!");
	}
	
	/*
	private static Formula arrumaTermosPorEquivalencia(List<Tupla<Formula, Tipo>> termos) throws Exception
	{
		Formula formulaAnterior = null;
		for(int i = 0, a = 0; i < termos.size(); i++)
		{
			if(termos.get(i).termo2 == Tipo.EQUIVALENCIA)
			{
				List<Tupla<Formula, Tipo>> sublista = termos.subList(a, i+1);
				sublista.get(i-a).termo2 = null;
				
				Formula f = arrumaTermosPorImplicacao(sublista);
				
				if(formulaAnterior == null)
				{
					formulaAnterior = f;
				}
				else
				{
					Formula ff = new Formula();
					ff.operacao = Tipo.EQUIVALENCIA;
					ff.esquerda = formulaAnterior;
					ff.direita = f;
					formulaAnterior = ff;
				}
				
				a = i+1;
			}
			else if(termos.get(i).termo2 == null) // chegamos no fim da lista de termos, hora de finalizar
			{
				List<Tupla<Formula, Tipo>> sublista = termos.subList(a, i+1);
				
				Formula f = arrumaTermosPorImplicacao(sublista);
				
				if(formulaAnterior == null) // nao teve nenhum termo encotrado antes da operacao
				{
					return f;
				}
				else
				{
					Formula ff = new Formula();
					ff.operacao = Tipo.EQUIVALENCIA;
					ff.esquerda = formulaAnterior;
					ff.direita = f;
					return ff;
				}
			}
		}
		throw new Exception("Erro ao organizar precedencia!");
	}
	*/
	
	
	private static Formula arrumaTermosPorPrecedencia(List<Tupla<Formula, Tipo>> termos) throws Exception
	{
		return arrumaTermosPorPrecedencia(termos, Tipo.EQUIVALENCIA);
	}
	
	private static Formula arrumaTermosPorPrecedencia(List<Tupla<Formula, Tipo>> termos, Tipo operacaoPrecedente) throws Exception
	{
		Formula formulaAnterior = null;
		
		if(operacaoPrecedente == Tipo.CONJUNCAO) // se for conjuncao, ja esta limpo de todos os outros termos menos precedentes
		{
			for(Tupla<Formula, Tipo> tupla : termos)
			{
				if(formulaAnterior == null)
				{
					formulaAnterior = tupla.termo1;
				}
				else
				{
					Formula f = new Formula();
					f.operacao = Tipo.CONJUNCAO;
					f.esquerda = formulaAnterior;
					f.direita = tupla.termo1;
					formulaAnterior = f;
				}
			}
			return formulaAnterior;
		}
		
		//se nao for conjuncao, vamos descobrir que sera o cara mais precedente apos o atual
		Tipo proximaOperacaoPrecedente = null;
		switch(operacaoPrecedente)
		{
			case EQUIVALENCIA:
				proximaOperacaoPrecedente = Tipo.IMPLICACAO;
				break;
			case IMPLICACAO:
				proximaOperacaoPrecedente = Tipo.DISJUNCAO;
				break;
			case DISJUNCAO:
				proximaOperacaoPrecedente = Tipo.CONJUNCAO;
				break;
			default:
				break;
		}
		
		for(int i = 0, a = 0; i < termos.size(); i++)
		{
			if(termos.get(i).termo2 == operacaoPrecedente)
			{
				List<Tupla<Formula, Tipo>> sublista = termos.subList(a, i+1);
				sublista.get(i-a).termo2 = null;
				
				Formula f = arrumaTermosPorPrecedencia(sublista, proximaOperacaoPrecedente);
				
				if(formulaAnterior == null)
				{
					formulaAnterior = f;
				}
				else
				{
					Formula ff = new Formula();
					ff.operacao = operacaoPrecedente;
					ff.esquerda = formulaAnterior;
					ff.direita = f;
					formulaAnterior = ff;
				}
				
				a = i+1;
			}
			else if(termos.get(i).termo2 == null) // chegamos no fim da lista de termos, hora de finalizar
			{
				List<Tupla<Formula, Tipo>> sublista = termos.subList(a, i+1);
				
				Formula f = arrumaTermosPorPrecedencia(sublista, proximaOperacaoPrecedente);
				
				if(formulaAnterior == null) // nao teve nenhum termo encotrado antes da operacao
				{
					return f;
				}
				else
				{
					Formula ff = new Formula();
					ff.operacao = operacaoPrecedente;
					ff.esquerda = formulaAnterior;
					ff.direita = f;
					return ff;
				}
			}
		}
		throw new Exception("Erro ao organizar precedencia!");
	}
	
	@Override
	public String toString()
	{
		__tab = "";
		return this.__toString();
	}

	private String __toString()
	{
		String str="";

		__tab += "-";
		
		if(this.operacao == Tipo.ATOMO)
		{
			str += "\n"+__tab + this.atomo;
		}
		else if(this.operacao == Tipo.NEGACAO)
		{
			str += "\n"+__tab + "NEGACAO";
			str += "\n"+__tab + this.esquerda.__toString();
		}
		else
		{
			str += "\n"+__tab + this.operacao.name();
			str += this.esquerda.__toString();
			str += this.direita.__toString();
		}
		
		__tab = __tab.substring(1);
		
		return str;
	}

}
